
\documentclass[preprint]{elsarticle}

%
%\usepackage{makeidx}  % allows for indexgeneration
\usepackage{packages}

\newcommand{\shortv}[1]{#1}
\newcommand{\longv}[1]{}%{#1}
%
%\newcommand{\choice}[1]{\widehat{#1}}
\renewcommand{\vspace}[1]{}
%\renewcommand{\small}{}
\usepackage{hyperref}
\usepackage{color}
\newcommand{\todo}[1]{\textcolor{red}{\textbf{#1}}}
\newcommand{\todoblue}[1]{\textcolor{blue}{\textbf{#1}}\\}
\newcommand{\add}[1]{\textcolor{blue}{\textbf{#1}}}
%\newcommand{\todo}[1]{}
%\newcommand{\todoblue}[1]{}


\title{Adaptable Processes \tnoteref{t1}}
\tnotetext[t1]{Supported 
by the French project ANR-2010-SEGI-013  - \textsc{Aeolus}, 
by the EU integrated project HATS, 
the Fondation de Coop\'eration Scientifique Digiteo Triangle de la Physique, 
by PEst-OE/EEI/UI0527/2011
Centro de Inform\'{a}tica e Tecnologias da Informa\c{c}\~{a}o (CITI/FCT/UNL) - 2011-2012, 
and by 
FCT / MCTES 
- Carnegie Mellon Portugal Program, grant NGN-44-2009-12
- \textsc{Interfaces}.}

\author[bol]{Mario Bravetti}
\ead{bravetti@cs.unibo.it}
\address[bol]{Laboratory Focus (University of Bologna/INRIA), Italy}

\author[gre]{Cinzia Di Giusto}
\ead{cinzia-digiusto@inrialpes.fr} 
\address[gre]{INRIA Rh\^{o}ne Alpes, France}

\author[lis]{Jorge A. P\'erez}
\ead{japerezp@gmail.com} 
\address[lis]{CITI, Department of Computer Science, FCT New University of Lisbon, Portugal}

\author[bol]{Gianluigi Zavattaro}
\ead{zavattar@cs.unibo.it}
 

\begin{document}
%

\begin{abstract}
%Deploying dynamically evolvable software applications is  a common practice nowadays.
%This is typically achieved by means of mechanisms capable of \emph{adapting} the system
%components to the modifications required by the external environment.
%{\em Correctness} and {\em evolvability} are closely related concerns: components might evolve 
%along time, possibly in reaction to errors, but it is most desirable that the overall 
%system exhibits a bounded or finite amount of error states.
%We propose a framework for reasoning about dynamically evolvable component
%systems. We introduce a basic calculus with evolvability capabilities 
%and propose two correctness properties: {\em bounded} and {\em eventual} adaptation. 
%While bounded adaptation ensures that at most $k$ errors will arise in future states---including those reachable as a result of dynamic reconfigurations---, eventual 
%adaptation ensures that the system will eventually reach a state from which no 
%other error will arise (i.e., only finitely many errors can occur). We study the 
%(un)decidability of these two adaptation properties in six different variants of the 
%calculus, which represent different evolvability patterns under structural and 
%behavioral criteria.
We propose the concept of \emph{adaptable processes} as a way of overcoming the limitations that process calculi have for describing patterns of dynamic \emph{process evolution}.
Such patterns rely on direct ways of controlling the behavior and location of \emph{running} processes, and so 
they are at the heart of the \emph{adaptation} capabilities present in many modern concurrent systems.
Adaptable processes have a location and are sensible to actions of \emph{dynamic update} at runtime; 
this allows to express a wide range of evolvability patterns for concurrent processes.
We introduce a core calculus of adaptable processes and propose two verification problems
for them: \emph{bounded} and \emph{eventual adaptation}.
While the former ensures that the number of consecutive erroneous
states that can be traversed during a computation is bound by some 
given number $k$,
%errors will arise in future states, 
the latter ensures that if the system 
%enters into an error state then it will eventually reach a correct state.
enters into a state with errors then a state without errors  will be eventually reached. 
We study the (un)decidability of these two problems in several variants of the calculus, which  
result from considering dynamic and static topologies of adaptable processes as well as different evolvability patterns.
Rather than a specification language, our calculus intends to be a basis for 
investigating the fundamental properties of evolvable processes and for 
developing richer languages with evolvability capabilities.
\end{abstract}

\begin{keyword}
Process Calculi \sep Expressiveness and Decidability \sep Dynamic Evolution \sep Adaptation \sep Evolvable Processes \sep Verification
\end{keyword}

% \institute{
%   Dipartimento di  Scienze dell'Informazione, Universit\`a di Bologna, Italy
% \and 
% INRIA Rh\^{o}ne-Alpes, Grenoble, France
% \and 
% CITI - FCT New University of Lisbon, Portugal
% }
\maketitle              % typeset the title of the contribution

%\vspace{-10mm}
%\newpage
%\input{todo}
\newpage
{\small
\tableofcontents
}

\newpage
 \section{Introduction}
     \input{introd}
%\newpage
 \section{A Calculus of Adaptable Processes}\label{s:calculi}
   \input{calculi}
   
 \section{Correctness Properties: Bounded and Eventual Adaptation}\label{s:prop}
   \input{properties}
 
 \section{Adaptable Processes, By Examples}\label{s:examp}
 \input{example}

 \section{Preliminaries}\label{s:prelim}
  \input{preliminaries}
% 
 \section{Undecidability Results for \evol{1}}\label{s:ev1}
  \input{evol1}
% 
 \section{(Un)decidability Results for \evol{2}}\label{s:ev2}
  \input{evol2}
% 
 \section{(Un)decidability Results for \evol{3}}\label{s:ev3}
 \input{evol3} 
% 
\section{Related Work and Discussion}\label{s:rw}


 \input{relatedwork}
 \input{discuss}

 \section{Concluding Remarks}\label{s:conc}
  \input{concl}
% 
% 
% 
 \bibliographystyle{model1b-num-names}
 \bibliography{referen,DSbib}
% 
%\end{document}
\appendix
\input{appendix}

\end{document}